(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
 Patrice Godefroid, SAGE (systematic dynamic test generation)
 For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun T4_28 () (_ BitVec 32))
(declare-fun T4_16 () (_ BitVec 32))
(declare-fun T4_4 () (_ BitVec 32))
(declare-fun T1_28 () (_ BitVec 8))
(declare-fun T1_29 () (_ BitVec 8))
(declare-fun T1_30 () (_ BitVec 8))
(declare-fun T1_31 () (_ BitVec 8))
(declare-fun T1_16 () (_ BitVec 8))
(declare-fun T1_17 () (_ BitVec 8))
(declare-fun T1_18 () (_ BitVec 8))
(declare-fun T1_19 () (_ BitVec 8))
(declare-fun T1_4 () (_ BitVec 8))
(declare-fun T1_5 () (_ BitVec 8))
(declare-fun T1_6 () (_ BitVec 8))
(declare-fun T1_7 () (_ BitVec 8))
(assert 
(let ((?v_5 (bvadd T4_16 (_ bv19 32))) (?v_4 (bvadd T4_28 (_ bv32 32)))) 
(let ((?v_3 (bvsub (_ bv65536 32) ?v_4)) (?v_2 (bvult (_ bv4 32) T4_4))) 
(let ((?v_0 (bvsub (_ bv0 32) ((_ zero_extend 24) (ite (bvult ?v_3 (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) 
(let ((?v_1 (bvule ?v_0 (_ bv0 32)))) (and true (= T4_4 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_7) (_ bv8 32)) ((_ zero_extend 24) T1_6)) (_ bv8 32)) ((_ zero_extend 24) T1_5)) (_ bv8 32)) ((_ zero_extend 24) T1_4))) (= T4_16 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_19) (_ bv8 32)) ((_ zero_extend 24) T1_18)) (_ bv8 32)) ((_ zero_extend 24) T1_17)) (_ bv8 32)) ((_ zero_extend 24) T1_16))) (= T4_28 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_31) (_ bv8 32)) ((_ zero_extend 24) T1_30)) (_ bv8 32)) ((_ zero_extend 24) T1_29)) (_ bv8 32)) ((_ zero_extend 24) T1_28))) (bvslt (bvadd T4_28 (_ bv29 32)) (_ bv0 32)) (bvule (bvadd T4_4 (_ bv8 32)) (_ bv573440 32)) ?v_1 (bvule (_ bv0 32) ?v_0) ?v_1 ?v_2 (not (= T4_4 (_ bv0 32))) ?v_2 (bvule (bvadd T4_16 (_ bv20 32)) (_ bv573440 32)) (bvult (_ bv4 32) T4_16) (bvule T4_16 (_ bv65516 32)) (not (= T4_16 (_ bv0 32))) (bvult (_ bv4 32) ?v_3) (bvule (_ bv4 32) ?v_3) (not (= ?v_3 (_ bv0 32))) (bvult ?v_3 (_ bv200000000 32)) (bvule ?v_5 (bvadd T4_4 (_ bv7 32))) (bvule (_ bv139327880 32) (bvadd T4_28 (_ bv141164648 32))) (bvult (_ bv0 32) ?v_4) (bvule (_ bv0 32) ?v_4) (bvule ?v_4 ?v_5) (bvule (bvadd T4_28 (_ bv31 32)) ?v_5) (= T4_28 (_ bv56 32)) (not (= T4_28 (_ bv0 32)))))))))
(check-sat)
(exit)
